(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(declare-fun j () Real)
(declare-fun k () Real)
(declare-fun l () Real)
(declare-fun m () Real)
(declare-fun n () Real)
(declare-fun o () Real)
(declare-fun p () Real)
(declare-fun q () Real)
(declare-fun r () Real)
(declare-fun u () Real)
(assert (not (exists ((s Real)) (=> (and (= i 0.0 (+ q (/ (- a l) a)) 0.0 l) (<= (- a l) (- 2.0 d (- u)))) (= (= (<= s 0.0) (<= 0.0 i (* d (- u)))) (= g 0.0))))))
(assert (not (exists ((t Real)) (=> (and (=> (<= 0.0 o) (<= (* (/ 2.0 c h) j) k)) (= (- b e) 1.0)) (= m 0.0 n k)))))
(assert (= b (+ e p) f (+ u p) 0.0 (/ i r)))
(check-sat)
